T, T':Type, x:Id, c:T, a:Id, P:(TT'Prop).
ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v))  MsgA 

latex

Definitions	if b t else f fi, p  q, eqof(d), false, x  dom(f), f(x), P  Q, MsgA, Prop, ma-single-pre-init1(x;T;c;a;T';y,v.P(y;v)), with ds: ds init: initaction a:T precondition a(v) is P, Top, State(ds), x : v, x. t(x), x(s1,s2), f(x)?z, t  T, IdDeq, Id, x:A. B(x)
Lemmas	fpf-cap-single1, fpf-single wf, id-deq wf, ma-state wf, Id wf, ma-single-pre-init wf, eqof eq btrue, bfalse wf, eqof wf, bor wf, ifthenelse wf